A, B:es_realizer{i:l}. R-compat{i:l}(A; B)  Prop{i'} 

latex

Definitions

R-interface-compat(A;B), x:AB(x), P & Q, Type, R-frame-compat(A;B), Rda(R), KindDeq, Knd, x. t(x), f || g, Rds(R), IdDeq, Id, s = t, b, A, b, , R-base-domain(R), p = q, x:AB(x), P  Q, Unit, left+right, R-loc(R), a = b, True, Rnone?(x1), #$n, n-m, , Rplus-right(x1), {x:A| B(x) }, Rplus-left(x1), {T}, Rplus?(x1), False, a<b, Void, , ij, -n, R-size(R), n+m, A || B, Prop, t  T, AB, P  Q, Realizer, x:A. B(x),

Lemmas

ge wf, nat properties, nat wf, le wf, Rplus? wf, R-size-decreases, Rplus-left wf, R-size wf, Rplus-right wf, nat plus wf, Rnone? wf, true wf, not functionality wrt iff, assert-eq-id, eq id wf, R-loc wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, eq bd wf, R-base-domain wf, bool wf, bnot wf, not wf, assert wf, es realizer wf, Id wf, id-deq wf, Rds wf, fpf-compatible wf, Knd wf, Kind-deq wf, Rda wf, R-frame-compat wf, R-interface-compat wf